$\forall$$n$:$\mathbb{N}$, $T$:Type, $R_{1}$,$R_{2}$:($T$$\rightarrow$$T$$\rightarrow$prop\{i:l\}).
\\[0ex]rel\_implies($T$; $R_{1}$; $R_{2}$) $\Rightarrow$ rel\_implies($T$; rel\_exp($T$; $R_{1}$; $n$); rel\_exp($T$; $R_{2}$; $n$))